(declare-fun a () Int)
(declare-fun b (Int Int) Int)
(declare-fun c (Int Int) Int)
(assert (forall ((d Int) (y Int)) (= (c d y) (div d y))))
(push)
(assert (= (c (b 3 (b 3 a)) 3) 0))
(check-sat)
(pop)
(check-sat)
(assert (= (c (b 3 (b 3 a)) 3) 0))
(check-sat)
